$\forall$$w$:World, ${\it rx}$, ${\it ra}$:(Id$\rightarrow$Id), ${\it rainv}$:(Id$\rightarrow$(Id+Unit)), ${\it rt}$:(Id$\rightarrow$Id), ${\it rtinv}$:(Id$\rightarrow$(Id+Unit)).
\\[0ex]inv{-}rel(Id;Id;${\it ra}$;${\it rainv}$)
\\[0ex]$\Rightarrow$ inv{-}rel(Id;Id;${\it rt}$;${\it rtinv}$)
\\[0ex]$\Rightarrow$ world{-}rename(${\it rx}$;${\it ra}$;${\it rt}$;${\it rainv}$;${\it rtinv}$;$w$) $\in$ World